Step of Proof: branch-ifthenelse
11,40
postcript
pdf
Inference at
*
1
1
I
of proof for Lemma
branch-ifthenelse
:
1.
b
:
2.
P
: Top
3.
Q
: Top
4.
x
:
b
5. bool-decider(
b
) = (inl
x
)
P
~ if
b
then
P
else
Q
fi
latex
by AutoBoolCase
b
latex
.
Definitions
left
+
right
,
Unit
,
P
Q
,
P
&
Q
,
x
:
A
B
(
x
)
,
x
:
A
B
(
x
)
,
,
s
=
t
,
b
,
b
,
x
:
A
.
B
(
x
)
,
t
T
,
,
A
,
P
Q
,
False
Lemmas
eqtt
to
assert
,
iff
transitivity
,
eqff
to
assert
,
assert
of
bnot
,
assert
wf
,
bnot
wf
,
not
wf
,
bool
wf
origin